/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.tester;

import gnu.getopt.Getopt;

import java.io.BufferedInputStream;
import java.io.BufferedReader;
import java.io.FileInputStream;
import java.io.FileReader;
import java.io.IOException;
import java.io.InputStream;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.StringTokenizer;
import java.util.TreeMap;

import alloy.api.AlloyRunner;
import alloy.api.SolutionData;
import alloy.api.TranslationException;
import alloy.ast.Command;
import alloy.ast.Commands;
import alloy.ast.FindCommand;
import alloy.type.ScopedType;
import alloy.util.CleanupManager;
import alloy.util.Dbg;
import alloy.util.EnvFailureException;
import alloy.util.ParamFormatException;
import alloy.util.Params;

/**
   Regression tester for the Alloy Analyzer.
*/

public class AlloyTester {

    private static final boolean DEBUG = true;
    
    /** Info message listener that prints progress/status messages
	while the tool is working. */
    private static Dbg.DbgMsgListener _infoListener = new Dbg.DbgMsgStreamPrinter(System.out);
    
    /** if <code>true</code>, verbose output enabled */
    private static boolean _verbose = false;

    /** help message */
    private static final String _helpMsg =
        "Alloy Tester command line options:\n" +
        "  -v : verbose output";

    
    public static void main(String[] args_) {
        try {
            Getopt g = new Getopt("Alloy Tester", args_, "v");
            int curOpt;
            while ((curOpt = g.getopt()) != -1) {
                switch (curOpt) {
                case 'v':
                    _verbose = true;
                    Dbg.addDbgMsgListener(Dbg.INFO, _infoListener);
                    break;
                case '?':
                case 'h':
                    System.out.println(_helpMsg);
                    return;
                }
            }
            Dbg.defaultInit();
            // NOTE: this doesn't work when this line is the first in the
            // method...a datarace?  or an issue with static initializers?
            Dbg.runningRegTests = true;
            for (int i = g.getOptind(); i < args_.length; i++) {
                try {
                    TestSpecs testSpecs = new TestSpecs(args_[i]);
                    if (DEBUG) System.out.println(testSpecs);
                    testSpecs.runTests();
                } catch (IOException e) {
                    System.err.println("Unable to open test spec. file "
                                       + args_[i]);
                }
            }
        } catch (RuntimeException e) {
            System.err.println("ERROR: Uncaught exception in regression tester.");
            e.printStackTrace();
            CleanupManager.exit(1);
        }
        CleanupManager.exit(0);
    }

    private static class TestSpecs {

        /** a List of configuration filenames to try */
        private List _configFilenames = new ArrayList(); // List[String]

        /** a Map from String model filenames to Booleans
            indicating whether the model should or should not
            compile */
        private Map _modelToCompileResult = new TreeMap(); // Map[String -> Boolean]

        public TestSpecs(String specFilename_) throws IOException {
            _parseSpecFile(specFilename_);
        }
        
        public void runTests() {
            Iterator configFileIter = _configFilenames.iterator();
            while (configFileIter.hasNext()) {
                String configFilename = (String)configFileIter.next();
                System.out.println("#####################################################");
                System.out.println("running with configuration file " + configFilename);
                System.out.println("#####################################################");
                try {
                    InputStream paramInput = new BufferedInputStream(new FileInputStream(configFilename));
                    Params.glob = Params.load(paramInput);
                } catch (IOException e) {
                    System.err.println("Could not load configuration file " + configFilename);
                    return;
                } catch (ParamFormatException e) {
                    System.err.println("Could not load configuration file " + configFilename);
                    return;
                }
                Iterator modelIter = _modelToCompileResult.keySet().iterator();
                while (modelIter.hasNext()) {
                    String modelFilename = (String)modelIter.next();
                    _runTestsForModel(modelFilename);
                    System.err.println("---------------------------------------------");
                }
            }
        }

        private void _runTestsForModel(String modelFilename) {
            System.out.println("compiling model " + modelFilename);
            // run garbage collection so garbage objects don't screw up
            // performance numbers
            System.gc();
            // first, prepare the spec
            boolean compiled = false;
            try {
                compiled = AlloyRunner.prepareSpec(modelFilename);
            } catch (RuntimeException e) {
                _failTest("tool crashed while compiling " + modelFilename + " with exception " + e);
                e.printStackTrace(System.out);
                return;
            }
            boolean shouldCompile = ((Boolean)_modelToCompileResult.get(modelFilename)).booleanValue();
            if (compiled && !shouldCompile) {
                _failTest("model " + modelFilename + " should not have compiled");
                return;
            }
            if (!compiled && shouldCompile) {
                _failTest("model " + modelFilename + " should have compiled");
                return;
            }
            if (compiled) {
                _passTest("model " + modelFilename + " compiled");
            } else {
                _passTest("model " + modelFilename + " did not compile");
                return;
            }
            // look for commands which have an expects declaration,
            // and map those commands to the expected result
            Map commandToResult = new HashMap(); // Map[Command -> Boolean]
            Map commandToSolData = new HashMap(); // Map[Command -> SolutionData]
            Commands commands = AlloyRunner.getCommands();
            Iterator commandIter = commands.getCommandIter();
            while (commandIter.hasNext()) {
                Command curCommand = (Command)commandIter.next();
                // translate every command to make sure it works
                try {
                    commandToSolData.put(curCommand, AlloyRunner.translateCommand((FindCommand)curCommand));
                } catch (TranslationException t_) {
                    System.out.println("Could not translate command " + curCommand.nodeString() + " of model " + modelFilename
                                       + ": " + t_);
                    continue;
                } catch (RuntimeException e_) {
                    _failTest("tool crash while translating command " + curCommand + " of model " + modelFilename + " with exception " + e_);
                    e_.printStackTrace(System.out);
                    continue;
                }
                if (curCommand instanceof FindCommand) {
                    FindCommand fCommand = (FindCommand)curCommand;
                    if (fCommand.info().hasExpects()) { //!fCommand.getExpects().isEmpty()) {
                        int expected = fCommand.info().expectsCount(); //fCommand.getExpects().getInt();
                        Boolean shouldHaveSol;
                        if (expected > 0) {
                            shouldHaveSol = new Boolean(true);
                        } else {
                            shouldHaveSol = new Boolean(false);
                        }
                        commandToResult.put(fCommand, shouldHaveSol);
                    }
                }
            }
            if (!Params.glob.getBoolParam("DEVEL", "regexec")) return;
            // run each command specified in the test file, and check if the result is what we expect
            commandIter = commands.getCommandIter();
            while (commandIter.hasNext()) {
                Command command = (Command)commandIter.next();
                // if it didn't translate, don't try to run it
                if (!commandToSolData.containsKey(command)) continue;
                // need to reset scopes
                // AlloyRunner has undocumented assumption that solution data passed
                // to analyzeCommand() came from last command passesd to translateCommand()
                ScopedType.setBasicTypeScopes(command);
                System.out.println("Analyzing command " + command);
                SolutionData solution = null;
                try {
                    AlloyRunner.clearState();
                    solution = AlloyRunner.analyzeCommand((SolutionData)commandToSolData.get(command),
                                                          System.currentTimeMillis());
                } catch (RuntimeException e) {
                    _failTest("tool crash while analyzing command " + command + " of model " + modelFilename + " with exception " + e);
                    e.printStackTrace(System.out);
                    // NOTE: here, do we need to recompile the spec?  I don't think so, but not sure
                    continue;
                }
                 catch (EnvFailureException e) {
                     _failTest("env failure while analyzing command " + command + " of model " + modelFilename + " with exception " + e);
                     e.printStackTrace(System.out);
//                     // NOTE: here, do we need to recompile the spec?  I don't think so, but not sure
                     continue;
                 }
                boolean foundSolution = (solution != null);
                if (commandToResult.containsKey(command)) {
                    boolean expectSolution = ((Boolean)commandToResult.get(command)).booleanValue();
                    if (foundSolution && !expectSolution) {
                        _failTest("command " + command + " of model " + modelFilename + " should have no solution, but solution found\n" + solution);
                        continue;
                    }
                    if (!foundSolution && expectSolution) {
                        _failTest("command " + command + " of model " + modelFilename + " should have a solution");
                        continue;
                    }
                    if (foundSolution) {
                        _passTest("solution found for command " + command + " of model " + modelFilename);
                    } else {
                        _passTest("no solution found for command " + command + " of model " + modelFilename);
                    }
                }
            }                        
            
        }
        
        private void _parseSpecFile(String specFilename_) throws IOException {
            BufferedReader specReader = new BufferedReader(new FileReader(specFilename_));
            // first line should have config files
            for (StringTokenizer configFileTokens = new StringTokenizer(specReader.readLine());
                 configFileTokens.hasMoreTokens(); ) {
                _configFilenames.add(configFileTokens.nextToken());
            }
            // rest of the lines specify test modules and expected results
            String currentLine;
            while ((currentLine = specReader.readLine()) != null) {
                StringTokenizer modelTestTokens = new StringTokenizer(currentLine);
                String modelFilename;
                Boolean shouldCompile;
                // first token is either the model filename, or an "n", indicating
                // the model shouldn't compile
                String firstToken = modelTestTokens.nextToken();
                if (firstToken.equals("n")) {
                    shouldCompile = new Boolean(false);
                    modelFilename = modelTestTokens.nextToken();
                } else {
                    shouldCompile = new Boolean(true);
                    modelFilename = firstToken;
                }
                _modelToCompileResult.put(modelFilename, shouldCompile);
            }
        }

        private void _failTest(String message) {
            System.out.println("FAIL: " + message);
        }

        private void _passTest(String message) {
            System.out.println("PASS: " + message);
        }
        
        public String toString() {
            return "config files: " + _configFilenames + ", tests: " + _modelToCompileResult;
        }
    }
        
}
